Inference at * 2 1 
Iof proof for Lemma nth tl is fseg:



1. T : Type
2. L1 : T List
3. L2 : T List
4. n : {0..(||L2||+1)}
5. L1 = nth_tl(n;L2)
  L2 = (firstn(n;L2) @ L1) 

latex

 by ((((((Symmetry) 
CollapseTHEN (HypSubst (-1) 0))) 
CollapseTHEN ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))) 
CollapseTHEN (((
CBackThruLemma `append_firstn_lastn`) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 2:n
C),(first_nat 3:n)) (first_tok :t) inil_term))))) 

latex

C.

Definitions	firstn(n;as), as @ bs, {i..j}, {i...j}, {x:A| B(x)} , A, False, P  Q, Void, n+m, i  j < k, P & Q, x:A  B(x), ||as||, x:A. B(x), x:AB(x), , nth_tl(n;as), a < b, A  B, , type List, Type, s = t, #$n, t  T
Lemmas	append wf, append firstn lastn, length wf1, le wf